Model Checking in Practice: An Analysis of the ACCESS.bus Protocol using SPIN

摘要

This paper presents a case study of the use of model checking foranalyzing an industrial protocol, the ACCESS.bus protocol. Our analysis ofthis protocol was carried out using SPIN, an automated verificationsystem which includes an implementation of model-checkingalgorithms. A model of the protocol was developed, and propertiesexpressed by linear-time temporal-logic formulas were checked on thismodel. This analysis revealed subtle flaws in the design of theprotocol. Developers who worked on implementations of ACCESS.bus wereunaware of these flaws at a very late stage of their developmentprocess. We also present suggestions for solving the detectedproblems.